Nuprl Lemma : l_intersection_wf
11,40
postcript
pdf
A
:Type,
eq
:EqDecider(
A
),
L1
,
L2
:(
A
List). l_intersection(
eq
;
L1
;
L2
)
(
A
List)
latex
Definitions
Type
,
t
T
,
x
:
A
.
B
(
x
)
,
EqDecider(
T
)
,
type
List
,
deq-member(
eq
;
x
;
L
)
,
x
.
A
(
x
)
,
filter(
P
;
l
)
,
l_intersection(
eq
;
L1
;
L2
)
Lemmas
filter
wf
,
deq-member
wf
,
deq
wf
origin
A:Type, eq:EqDecider(A), L1, L2:(A List). l_intersection(eq;L1;L2) 
(A List) A:Type, eq:EqDecider(A), L1, L2:(A List). l_intersection(eq;L1;L2) (A List) Tx:A. B(x)
x.A(x)